a  n
== if 0 z a then a  n if ((-a) rem n = 0) then -((-a)  n) else (-((-a)  n))+(-1) fi  

latex

Up	int 2, int 2
Wellformedness Lemmas	div floor wf, div floor wf
Definitions	i z j, if b then t else f fi , (i = j), n rem m, n+m, n  m, -n, #$n
FDL editor aliases	div_floor